﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Logic
{
	class Sentence
	{
		readonly string[] operatorList = { "&", "|", "=>", "<=>" };

		int? symbolID;
		List<Sentence> terms;
		List<LogicalSystem.BinaryOperators> operators;
		LogicalSystem logicalSystem;		
		public bool IsNegative;		

		public override string ToString()
		{
            if (symbolID != null)
                return (IsNegative ? "~" : "") + logicalSystem.Symbols[symbolID.Value];
            else
            {
                StringBuilder sb = new StringBuilder();
                if (IsNegative) sb.Append("~");
                sb.Append('(');
                for (int i = 0; i < terms.Count - 1; i++)
                {                    
                    sb.Append(terms[i].ToString());                    
                    sb.Append(' ');
                    sb.Append(operatorList[(int)operators[i]]);
                    sb.Append(' ');
                }
                sb.Append(terms[terms.Count - 1].ToString());
                sb.Append(')');

                return sb.ToString();
            }				
		}

		public Sentence()
		{
		}

		public Sentence(LogicalSystem ls, int symbolID, bool isNegative)
		{
			logicalSystem = ls;
			this.symbolID = symbolID;
			IsNegative = isNegative;
		}

		public Sentence(LogicalSystem ls, string s) : this(ls, s, 0, s.Length, false)
		{
			
		}
		public Sentence(LogicalSystem ls, string s, int start, int end, bool negative)
		{
			logicalSystem = ls;						
			IsNegative = negative;

			int i = start;
			bool nextIsNegated = false;
			bool lastIsOp = true;
			terms = new List<Sentence>();
			operators = new List<LogicalSystem.BinaryOperators>();

			do
			{
				if (lastIsOp)
				{					
					switch (s[i])
					{
						case '~':
							nextIsNegated = !nextIsNegated;
							break;
						case '(':
							int br = 1, ci;
							for (ci = i + 1; br > 0; ci++) if (s[ci] == '(') br++; else if (s[ci] == ')') br--;							
							terms.Add(new Sentence(ls, s, i + 1, ci - 1, nextIsNegated));
							lastIsOp = nextIsNegated = false;							
							i = ci;
							break;
						case ' ':
							break;
						default:							
							int li = s.IndexOf(' ', i);
							if (li == -1 || li > end) li = end;								
							string symbol = s.Substring(i, li - i);
							int symbolId = ls.Symbols.IndexOf(symbol);
							if (symbolId == -1)
								throw new Exception("Syntax error");
							terms.Add(new Sentence(ls, symbolId, nextIsNegated));
							lastIsOp = nextIsNegated = false;							
							i = li;
							break;
					}
					i++;
				}
				else
				{
                    if (s[i] == ' ') { i++; continue; }
                    int j;
					for(j = 0; j < operatorList.Length; j++)
					{
						string op =  operatorList[j];
                        if (String.Compare(s, i, op, 0, op.Length) == 0)
                        {
                            operators.Add((LogicalSystem.BinaryOperators)j);
                            i += op.Length;
                            break;
                        }                        
					}
                    if (j == operatorList.Length)
                        throw new Exception("Syntax error");
					lastIsOp = true;
				}
			} while (i < end);

			TryConvertSingleTerm();
		}

		public Sentence(LogicalSystem ls, IEnumerable<Sentence> terms, IEnumerable<LogicalSystem.BinaryOperators> ops, bool negative = false)
		{
			logicalSystem = ls;
			this.terms = terms.ToList();
			this.operators = ops.ToList();
            this.IsNegative = negative;
			TryConvertSingleTerm();
		}

		void TryConvertSingleTerm()
		{
			if (operators.Count == 0)
			{
				Sentence term = terms[0];
                if (term.symbolID == null)
                {
                    this.operators = term.operators;
                    this.terms = term.terms;
                }
                else
                {
                    this.symbolID = term.symbolID;
                    this.terms.Clear();
                }

				this.IsNegative = term.IsNegative ^ this.IsNegative;							
			}
		}

        Sentence[] Split(int k, bool negateFirst, bool negateSecond)
        {
            return new[] {
                    new Sentence(logicalSystem,
                        terms.GetRange(0, k + 1),
                        operators.GetRange(0, k), negateFirst),
                    new Sentence(logicalSystem,
                        terms.GetRange(k + 1, terms.Count - (k + 1)),
                        operators.GetRange(k + 1, operators.Count - (k + 1)), negateSecond)
                };
        }

        Sentence[] BinarySplitByOperator(LogicalSystem.BinaryOperators op, bool negateFirst = false, bool negateSecond = false)
        {
            int k = operators.IndexOf(op);
            if (k == -1) return null;
            else
                return Split(k, negateFirst, negateSecond);
        }

		public Sentence BicondEliminate()
		{
            if (symbolID != null)
                return this;

            List<Sentence> newTerms;
            List<LogicalSystem.BinaryOperators> newOps = this.operators;

            var split = BinarySplitByOperator(LogicalSystem.BinaryOperators.IfAndOnlyIf);
            if(split != null)
            {			
                Sentence AImpliesB = new Sentence(logicalSystem, new[] { split[0].BicondEliminate(), split[1].BicondEliminate() }, new[] { LogicalSystem.BinaryOperators.Implies });
                Sentence BImpliesA = new Sentence(logicalSystem, new[] { split[1].BicondEliminate(), split[0].BicondEliminate() }, new[] { LogicalSystem.BinaryOperators.Implies });

                newTerms = new List<Sentence>() { AImpliesB, BImpliesA };
                newOps = new List<LogicalSystem.BinaryOperators>() { LogicalSystem.BinaryOperators.And };                
			}
            else
            {
                newTerms = new List<Sentence>();
                for (int i = 0; i < terms.Count; i++)
                    newTerms.Add(terms[i].BicondEliminate());
            }

            return new Sentence(logicalSystem, newTerms, newOps, IsNegative);
		}

        public Sentence ImplEliminate()
        {
            if (symbolID != null)
                return this;

            List<Sentence> newTerms;
            List<LogicalSystem.BinaryOperators> newOps = this.operators;

            var split = BinarySplitByOperator(LogicalSystem.BinaryOperators.Implies, true, false);

			if(split != null)            
            {
                newTerms = new List<Sentence>() { split[0].ImplEliminate(), split[1].ImplEliminate() };
                newOps = new List<LogicalSystem.BinaryOperators>() { LogicalSystem.BinaryOperators.Or };
            }
            else
            {
                newTerms = new List<Sentence>();
                for (int i = 0; i < terms.Count; i++)
                    newTerms.Add(terms[i].ImplEliminate());
            }

            return new Sentence(logicalSystem, newTerms, newOps, IsNegative);
        }

        public Sentence DeMorgan()
        {
            if (symbolID != null)
                return this;

            List<Sentence> newTerms;
            List<LogicalSystem.BinaryOperators> newOps = this.operators;

            if (IsNegative)
            {    
                var split = BinarySplitByOperator(LogicalSystem.BinaryOperators.Or, true, true);
                if(split != null)
                {
                    newTerms = new List<Sentence>() { split[0].DeMorgan(), split[1].DeMorgan() };
                    newOps = new List<LogicalSystem.BinaryOperators>() { LogicalSystem.BinaryOperators.And };
                }
                else
                {
                    if (operators[0] != LogicalSystem.BinaryOperators.And)
                        throw new Exception("Can't apply De Morgan when there are not only & and |");

                    split = BinarySplitByOperator(LogicalSystem.BinaryOperators.And, true, true);

                    newTerms = new List<Sentence>() { split[0].DeMorgan(), split[1].DeMorgan() };                    
                    newOps = new List<LogicalSystem.BinaryOperators>() { LogicalSystem.BinaryOperators.Or };                    
                }
            }
            else
            {
                newTerms = new List<Sentence>();
                for (int i = 0; i < terms.Count; i++)
                    newTerms.Add(terms[i].DeMorgan());
            }

            return new Sentence(logicalSystem, newTerms, newOps, false);
        }

        public CNFSentence ConvertToCNF()
        {
            List<List<int>> formula = new List<List<int>>();
            if (symbolID != null)
            {
                int value = symbolID.Value;
                if(IsNegative)
                    value = ~value;
                formula.Add(new List<int>(new[] { value }));
                return new CNFSentence(logicalSystem, formula);
            }

            var split = BinarySplitByOperator(LogicalSystem.BinaryOperators.Or);
            if (split == null)
            {
                split = BinarySplitByOperator(LogicalSystem.BinaryOperators.And);
                formula.AddRange(split[0].ConvertToCNF().Formula);
                formula.AddRange(split[1].ConvertToCNF().Formula);
            }
            else
            {
                List<List<int>> l1 = split[0].ConvertToCNF().Formula;
                List<List<int>> l2 = split[1].ConvertToCNF().Formula;

                for(int i1 = 0; i1 < l1.Count; i1++)
                    for (int i2 = 0; i2 < l2.Count; i2++)                    
                        formula.Add(l1[i1].Concat(l2[i2]).ToList());                    
            }

            return new CNFSentence(logicalSystem, formula);
        }
	}
}
